Problem:
 active(nats()) -> mark(adx(zeros()))
 active(zeros()) -> mark(cons(0(),zeros()))
 active(incr(cons(X,Y))) -> mark(cons(s(X),incr(Y)))
 active(adx(cons(X,Y))) -> mark(incr(cons(X,adx(Y))))
 active(hd(cons(X,Y))) -> mark(X)
 active(tl(cons(X,Y))) -> mark(Y)
 active(adx(X)) -> adx(active(X))
 active(incr(X)) -> incr(active(X))
 active(hd(X)) -> hd(active(X))
 active(tl(X)) -> tl(active(X))
 adx(mark(X)) -> mark(adx(X))
 incr(mark(X)) -> mark(incr(X))
 hd(mark(X)) -> mark(hd(X))
 tl(mark(X)) -> mark(tl(X))
 proper(nats()) -> ok(nats())
 proper(adx(X)) -> adx(proper(X))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(incr(X)) -> incr(proper(X))
 proper(s(X)) -> s(proper(X))
 proper(hd(X)) -> hd(proper(X))
 proper(tl(X)) -> tl(proper(X))
 adx(ok(X)) -> ok(adx(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 incr(ok(X)) -> ok(incr(X))
 s(ok(X)) -> ok(s(X))
 hd(ok(X)) -> ok(hd(X))
 tl(ok(X)) -> ok(tl(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 10
  enrichment: match
  automaton:
   final states: {14,13,12,11,10,9,8,7,6}
   transitions:
    ok9(204) -> 181*
    ok9(206) -> 177*
    03() -> 60*
    top10(207) -> 14*
    zeros3() -> 57*
    active10(206) -> 207*
    ok4(74) -> 82*
    ok4(73) -> 81*
    ok4(63) -> 50*
    cons4(60,57) -> 63*
    cons4(82,81) -> 69*
    cons4(74,73) -> 75*
    adx4(65) -> 72*
    adx4(62) -> 50*
    adx4(57) -> 63*
    active4(41) -> 62*
    active4(63) -> 68*
    top4(68) -> 14*
    mark3(65) -> 62*
    mark4(75) -> 69*
    mark4(72) -> 50*
    adx5(75) -> 79*
    adx5(69) -> 68*
    active5(100) -> 86*
    active5(57) -> 69*
    proper4(60) -> 82*
    proper4(72) -> 68*
    proper4(57) -> 81*
    04() -> 74*
    zeros4() -> 73*
    proper5(65) -> 69*
    proper5(79) -> 86*
    proper5(74) -> 92*
    proper5(73) -> 91*
    active0(5) -> 6*
    active0(2) -> 6*
    active0(4) -> 6*
    active0(1) -> 6*
    active0(3) -> 6*
    mark5(79) -> 68*
    nats0() -> 1*
    top5(86) -> 14*
    mark0(5) -> 2*
    mark0(2) -> 2*
    mark0(4) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    adx6(87) -> 86*
    adx6(96) -> 142*
    adx6(93) -> 100*
    adx6(73) -> 103*
    adx0(5) -> 7*
    adx0(2) -> 7*
    adx0(4) -> 7*
    adx0(1) -> 7*
    adx0(3) -> 7*
    proper6(105) -> 112*
    proper6(75) -> 87*
    zeros0() -> 3*
    ok5(97) -> 124,92
    ok5(96) -> 129,91
    ok5(93) -> 69*
    cons0(3,1) -> 12*
    cons0(3,3) -> 12*
    cons0(3,5) -> 12*
    cons0(4,2) -> 12*
    cons0(4,4) -> 12*
    cons0(5,1) -> 12*
    cons0(5,3) -> 12*
    cons0(5,5) -> 12*
    cons0(1,2) -> 12*
    cons0(1,4) -> 12*
    cons0(2,1) -> 12*
    cons0(2,3) -> 12*
    cons0(2,5) -> 12*
    cons0(3,2) -> 12*
    cons0(3,4) -> 12*
    cons0(4,1) -> 12*
    cons0(4,3) -> 12*
    cons0(4,5) -> 12*
    cons0(5,2) -> 12*
    cons0(5,4) -> 12*
    cons0(1,1) -> 12*
    cons0(1,3) -> 12*
    cons0(1,5) -> 12*
    cons0(2,2) -> 12*
    cons0(2,4) -> 12*
    cons5(74,73) -> 93*
    cons5(92,91) -> 87*
    00() -> 4*
    ok6(100) -> 68*
    ok6(142) -> 123*
    ok6(139) -> 134*
    ok6(146) -> 122*
    ok6(101) -> 87*
    ok6(143) -> 180,138
    incr0(5) -> 8*
    incr0(2) -> 8*
    incr0(4) -> 8*
    incr0(1) -> 8*
    incr0(3) -> 8*
    05() -> 97*
    s0(5) -> 13*
    s0(2) -> 13*
    s0(4) -> 13*
    s0(1) -> 13*
    s0(3) -> 13*
    zeros5() -> 96*
    hd0(5) -> 9*
    hd0(2) -> 9*
    hd0(4) -> 9*
    hd0(1) -> 9*
    hd0(3) -> 9*
    cons6(74,103) -> 104*
    cons6(97,96) -> 101*
    cons6(97,142) -> 146*
    tl0(5) -> 10*
    tl0(2) -> 10*
    tl0(4) -> 10*
    tl0(1) -> 10*
    tl0(3) -> 10*
    ok7(150) -> 112*
    ok7(147) -> 175,133
    ok7(109) -> 86*
    ok7(186) -> 174*
    ok7(151) -> 131*
    ok7(193) -> 189*
    ok7(195) -> 192*
    proper0(5) -> 11*
    proper0(2) -> 11*
    proper0(4) -> 11*
    proper0(1) -> 11*
    proper0(3) -> 11*
    adx7(129) -> 123*
    adx7(119) -> 112*
    adx7(101) -> 109*
    adx7(96) -> 116*
    adx7(143) -> 147*
    adx7(180) -> 175*
    ok0(5) -> 5*
    ok0(2) -> 5*
    ok0(4) -> 5*
    ok0(1) -> 5*
    ok0(3) -> 5*
    active6(109) -> 112*
    active6(93) -> 87*
    top0(5) -> 14*
    top0(2) -> 14*
    top0(4) -> 14*
    top0(1) -> 14*
    top0(3) -> 14*
    mark6(105) -> 86*
    top1(36) -> 14*
    incr6(104) -> 105*
    active1(5) -> 36*
    active1(2) -> 36*
    active1(4) -> 36*
    active1(1) -> 36*
    active1(3) -> 36*
    top6(112) -> 14*
    proper1(5) -> 36*
    proper1(2) -> 36*
    proper1(4) -> 36*
    proper1(1) -> 36*
    proper1(3) -> 36*
    incr7(142) -> 153*
    incr7(122) -> 112*
    incr7(117) -> 118*
    incr7(146) -> 150*
    ok1(25) -> 25,9
    ok1(20) -> 36,11
    ok1(15) -> 36,11
    ok1(29) -> 36,11
    ok1(24) -> 24,8
    ok1(31) -> 31,12
    ok1(21) -> 21,7
    ok1(33) -> 33,13
    ok1(28) -> 28,10
    proper7(104) -> 122*
    proper7(74) -> 124*
    proper7(96) -> 180*
    proper7(118) -> 128*
    proper7(103) -> 123*
    proper7(73) -> 129*
    tl1(5) -> 28*
    tl1(2) -> 28*
    tl1(4) -> 28*
    tl1(1) -> 28*
    tl1(3) -> 28*
    active7(150) -> 128*
    active7(101) -> 119*
    hd1(5) -> 25*
    hd1(2) -> 25*
    hd1(4) -> 25*
    hd1(1) -> 25*
    hd1(3) -> 25*
    mark7(155) -> 128*
    mark7(118) -> 112*
    s1(5) -> 33*
    s1(2) -> 33*
    s1(4) -> 33*
    s1(1) -> 33*
    s1(3) -> 33*
    cons7(124,123) -> 122*
    cons7(139,147) -> 151*
    cons7(154,153) -> 155*
    cons7(97,116) -> 117*
    incr1(5) -> 24*
    incr1(2) -> 24*
    incr1(4) -> 24*
    incr1(1) -> 24*
    incr1(3) -> 24*
    top7(128) -> 14*
    cons1(3,1) -> 31*
    cons1(3,3) -> 31*
    cons1(3,5) -> 31*
    cons1(4,2) -> 31*
    cons1(4,4) -> 31*
    cons1(5,1) -> 31*
    cons1(5,3) -> 31*
    cons1(5,5) -> 31*
    cons1(20,15) -> 16*
    cons1(1,2) -> 31*
    cons1(1,4) -> 31*
    cons1(2,1) -> 31*
    cons1(2,3) -> 31*
    cons1(2,5) -> 31*
    cons1(3,2) -> 31*
    cons1(3,4) -> 31*
    cons1(4,1) -> 31*
    cons1(4,3) -> 31*
    cons1(4,5) -> 31*
    cons1(5,2) -> 31*
    cons1(5,4) -> 31*
    cons1(1,1) -> 31*
    cons1(1,3) -> 31*
    cons1(1,5) -> 31*
    cons1(2,2) -> 31*
    cons1(2,4) -> 31*
    incr8(147) -> 166*
    incr8(151) -> 159*
    incr8(131) -> 128*
    incr8(175) -> 173*
    adx1(15) -> 16*
    adx1(5) -> 21*
    adx1(2) -> 21*
    adx1(4) -> 21*
    adx1(1) -> 21*
    adx1(3) -> 21*
    proper8(155) -> 162*
    proper8(142) -> 175*
    proper8(117) -> 131*
    proper8(97) -> 134*
    proper8(154) -> 174*
    proper8(116) -> 133*
    proper8(96) -> 138*
    proper8(153) -> 173*
    proper8(143) -> 192*
    01() -> 20*
    cons8(186,166) -> 201*
    cons8(134,133) -> 131*
    cons8(174,173) -> 162*
    cons8(167,166) -> 168*
    zeros1() -> 15*
    06() -> 139*
    nats1() -> 29*
    adx8(192) -> 188*
    adx8(138) -> 133*
    adx8(195) -> 200*
    mark1(25) -> 25,9
    mark1(24) -> 24,8
    mark1(21) -> 21,7
    mark1(16) -> 36,6
    mark1(28) -> 28,10
    zeros6() -> 143*
    top2(38) -> 14*
    ok8(197) -> 182*
    ok8(159) -> 128*
    ok8(201) -> 162*
    ok8(166) -> 173*
    ok8(200) -> 188*
    active2(20) -> 38*
    active2(15) -> 38*
    active2(29) -> 38*
    active8(159) -> 162*
    active8(146) -> 131*
    proper2(20) -> 47*
    proper2(15) -> 46*
    proper2(16) -> 38*
    s7(97) -> 154*
    s7(139) -> 186*
    cons2(47,46) -> 38*
    cons2(43,41) -> 42*
    top8(162) -> 14*
    adx2(46) -> 38*
    adx2(41) -> 42*
    incr9(169) -> 162*
    incr9(188) -> 181*
    incr9(200) -> 204*
    mark2(42) -> 38*
    active9(201) -> 177*
    active9(151) -> 169*
    02() -> 43*
    mark8(168) -> 162*
    zeros2() -> 41*
    s8(139) -> 167*
    s8(134) -> 174*
    s8(193) -> 197*
    top3(50) -> 14*
    top9(177) -> 14*
    proper3(42) -> 50*
    proper3(41) -> 51*
    proper3(43) -> 54*
    proper9(167) -> 182*
    proper9(147) -> 188*
    proper9(139) -> 189*
    proper9(166) -> 181*
    proper9(168) -> 177*
    ok2(41) -> 46*
    ok2(43) -> 47*
    cons9(197,204) -> 206*
    cons9(182,181) -> 177*
    ok3(60) -> 54*
    ok3(55) -> 38*
    ok3(57) -> 51*
    s9(189) -> 182*
    cons3(43,41) -> 55*
    cons3(60,57) -> 65*
    cons3(54,51) -> 50*
    07() -> 193*
    adx3(51) -> 50*
    adx3(41) -> 55*
    zeros7() -> 195*
    active3(55) -> 50*
  problem:
   
  Qed